#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"

int foo(int a, int b) {
	//int c=klee_change(a+b,b+a);
	
	
	return klee_change(a+b,a-b);

}

int main(int argc, char *argv[]) {

    int a=  argv[1][0] - '0';
    int b = argv[2][0] - '0';
	
    
    foo(a,b);
    return 0;
}
